i:. |i| = i   

latex

ProofTree

Definitions	True, ff, if b then t else f fi , , tt, t  T, False, P  Q, A, A  B, x:A. B(x),
Lemmas	nat wf, bnot wf, lt int wf, le wf, assert wf, bool wf, le int wf